\begin{tabbing}
@$i$ locl($a$) occurs once
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$$e$@$i$.es{-}kind(${\it es}$; $e$) = locl($a$)\+
\\[0ex]$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]${\it e'}$.((es{-}kind(${\it es}$; $e$) = locl($a$))
\\[0ex]$\Rightarrow$ (es{-}kind(${\it es}$; ${\it e'}$) = locl($a$))
\\[0ex]$\Rightarrow$ ($e$ = ${\it e'}$))))
\-\-\-
\end{tabbing}